perm filename CIRCUM.NOT[F83,JMC]2 blob sn#735297 filedate 1983-12-13 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	circum.not[f83,jmc]	Notes for circum[f83,jmc]
C00010 ENDMK
C⊗;
circum.not[f83,jmc]	Notes for circum[f83,jmc]

	The result of circumscribing ⊗ab is always a second order
formula because of the quantifier %2∀ab'%1.  However, in the examples
given so far in this paper, the formula is always equivalent to a
first order formula.  Appropriate substitutions for ⊗ab' can be
found to get this formula.  Vladimir Lifschitz (1983) has shown
when ⊗A(P) can be written in prenex form with only universal
quantifiers and no functions, then ⊗A'(P) is always equivalent
to a first order formula.  This result cannot simply be cited
here, because there are functions, namely the aspects.

	However, we can make a heuristic argument (which I hope
will be replaced by a proof) that
what gives trouble is not the functions or existential quantifiers
per se, but rather the possibility of using them to generate
an infinite set of elements satisfying ⊗ab.  This is essentially why the
axiom schema of mathematical induction cannot be reduced to a single formula.
However, iterating the aspect functions does not give anything which
can be proved to satisfy ⊗ab.  

	Even when ⊗A(P) reduces to a first order formula, in general
the formula will involve disjunctions.  This is the case for the
Reiter examples involving Nixon and the city of residence.  However,
in the bird and blocks world examples, we do better.  The first
order formula is obtained by a single substitution for ⊗ab', and
doesn't involve disjunction.

	One might suppose that this would correspond to there being
a unique minimal model, but this doesn't seem to be the case.
It seems rather to be some kind of relative minimal model.  There are
different models with different kinds of birds, but once the interpretations
of the predicates ⊗bird, ⊗ostrich, etc. are fixed, the interpretation
of the variable predicates ⊗ab and ⊗flies are determined uniquely by
circumscribing ⊗ab_z.  One goal in formulating an axiom system
is to achieve unique interpretations of the variable predicates.

	The way we have treated the bird example is a
reformulation in logic of what is often done by
inheritance of properties in ⊗is-a hierarchies.

IT IS NOT PRESENTLY CLEAR WHETHER WE CAN DO EVERYTHING NORMALLY
DONE WITH IS-A HIERARCHIES.

LOGIC AND PSEUDO-LOGIC, STRIPS AND ITS DISCONTENTS.

STANDARDLY NOT USUALLY

CHECK KEITH CLARK WORK AND SEE IF CIRCUMSCRIPTION DOES MORE THAN
PREDICATE COMPLETION.  CHECK HORN CLAUSE CASE.


1983 Dec 9

	The use of an abnormality function of situations whose value
we minimize may be more general then minimizing ab(aspects).
Here's the axiom

A'(P) ≡ A(P) ∧ ∀P'.A(P') ∧ ¬(abnormality(P') < abnormality(P)).

The only problem is to write the abnormality function.  Its range
would most generally be a partially ordered set.  Perhaps there is
no loss of generality in making it a segment of the ordinal numbers.
There is a loss of generality unless the poset has the property that
every subset has a minimal element.  Then there probably isn't.

The trouble with abnormality functions is that they aren't sufficiently
modular.  Namely, it looks like we have to assign abnormalities at
one time to the whole class of situations.

%3Etherington, David W. and Raymond Reiter (1983)%1: "On Inheritance
Hierarchies with Exceptions", in %2Proceedings of the National
Conference on Artificial Intelligence, AAAI-83%1, William Kaufman, Inc.

1983 Dec 13

Can we do finitization, i.e. getting finite models for situations,
by circumscription?  Here's the way.

We begin with certain objects already regarded as relevant to the
problem being dealt with.  Ohher objects are generated by relations
deemed relevant.  In contrast to search processes wehere we are
looking widely for an answer and where looking too widely only
wastes time, we are trying to keep things as narrow as possible, and
looking too widely may prevent getting a finite model.  Therefore,
we msut have a strong reason to deem a connection relevant.  The
circumscription expresses the conjecture that the only relevant
objects and facts are those generated by the process.  The goal of
the process is a finite model, e.g. the (m c b) triplet model of
missionaries and cannibals.  If the finite model leads to a solution,
in its micro-world, more facts may become relevant to validate the
solution or repair it.  If there is no solution in the model, then
we need to "think of" new methods and facts and redo the circumscription.